COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	\input jmclet
C00005 ENDMK
C⊗;
\input jmclet
\jmclet
\address
EMST Search Committee
Graduate School of Education
University of California, Berkeley
Berkeley, CA 94720
\body

Gentlemen:

	Martin Davis is one of the best known logicians in America,
and I am not qualified to evaluate his logical work.  However, I
know something of his work in areas touching computing and
artificial intelligence.

	He and Hilary Putnam wrote one of the first theorem proving
programs for predicate calculus, and the Davis-Putnam algorithm was
the benchmark in this field for a number of years.  More recently,
he has been developing a theory of adequate test data for program
debugging that uses the Chaitin-Kolmogorov theory of complexity.  Such
work requires someone of Davis's logical and mathematical knowledge
and sophistication.

	A third contribution was in clarifying the mathematical
structure of non-monotonic reasoning.  He was the first
mathematical logician to take an interest in these problems,
and his 1980 article in @p[Artificial Intelligence] was an
island of rigor and clarity in a sea of intuitive ideas.
Subsequently the topic is became relatively popular among logicians,
and I wish Davis had continued to work in it.

	His paper at the International Joint Conference
on Artificial Intelligence about the notion of "obvious deduction"
was done while he was visiting the Stanford Artificial Intelligence
Laboratory.  It may prove an important tool in making interactive
theorem provers practical.

	I don't know much about his educational work except that his
textbooks in computability and in non-standard analysis are well
regarded.

\closing
Sincerely,
John McCarthy
Professor
\endletter
\end